the_es:ES, e, e', y:E. e' before y  before(e)  (e' <loc y) 

latex

Definitions

ij, i<j, hd(l), (x  l), A & B, i  j < k, L1  L2, T, True, increasing(f;k), S  T, S  T, l[i], , {i..j}, ||as||, t  ...$L, ij, AB, x:A. B(x), pred(e), as @ bs, Dec(P), P  Q, P  Q, False, WellFnd{i}(A;x,y.R(x;y)), x. t(x), {T}, x before y  l, E, before(e), (e <loc e'), ES, Unit, P  Q, P & Q, P  Q, first(e), , Prop, b, A, t  T, b, x:A. B(x)

Lemmas

assert wf, not wf, bnot wf, bool wf, es-first wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, event system wf, es-locl wf, es-before wf, l before wf, es-E wf, es-locl-wellfnd, false wf, nil before, implies functionality wrt iff, all functionality wrt iff, es-pred wf, decidable es-E equal, append wf, member-es-before, length append, non neg length, length cons, length nil, length wf1, select wf, int seg wf, increasing wf, true wf, squash wf, le wf, select append front, es-pred-locl, l before append front, nil member, or functionality wrt iff, not functionality wrt iff, l member wf, cons member